A modifier to refer to the value of the <expression> at the time of

entry into a method.

(\forall <decl>; <range-exp>; <body-exp>)

The universal quantifier.

(\exists <decl>; <range-exp>; <body-exp>)

The existential quantifier.

a ==> b

a implies b

a <== b

a is implied by b

a <==> b

a if and only if b

as well as standard Java syntax for logical and, or, and not. JML

annotations also have access to Java objects, object methods and

operators that are within the scope of the method being annotated and

that have appropriate visibility. These are combined to provide formal

specifications of the properties of classes, fields and methods. For

example, an annotated example of a simple banking class may look like

public class BankingExample

{

public static final int MAX_BALANCE = 1000;

private /*@ spec_public @*/ int balance;

private /*@ spec_public @*/ boolean isLocked = false;

//@ public invariant balance >= 0 && balance <= MAX_BALANCE;

//@ assignable balance;

//@ ensures balance == 0;

public BankingExample()

{

this.balance = 0;

}

//@ requires 0 < amount && amount + balance < MAX_BALANCE;

//@ assignable balance;

//@ ensures balance == \old(balance) + amount;

public void credit(final int amount)

{

this.balance += amount;

}

//@ requires 0 < amount && amount <= balance;